package cwb
import scala.collection.mutable.HashMap

import agent.Agent
import agent.Action


/**
 * An ActList is represented by an action and its list of successors.
 */
class ActList(a: Action, v: List[Vertex]) {
  val act = a
      private var _vlist = v

      def vlist = _vlist

      def vlist_=(vlist: List[Vertex]) = _vlist = vlist


}

class Vertex(ag: Agent, s: List[ActList], w: List[ActList]) {
  val keycopy = ag
      private var _suc = s
      private var _wsuc = w

      def suc = _suc
      def suc_=(suc: List[ActList]) = _suc = suc
      def wsuc = _wsuc
      def wsuc_=(wsuc: List[ActList]) = _wsuc = wsuc
}

abstract class State[T] {
  var keycopy: Agent = null
      var id: Int = -10
      var prdiv: Boolean = false
      var gldiv: Boolean = false
      var mark: Boolean = false
      var pid: Int = -10
}

class AgentState() extends State[Agent] {
  private var _suc: List[(Action, List[AgentState])] = List()
      private var _taus: List[AgentState] = List()
      private var _newtaus: List[AgentState] = List()

      def suc = _suc
      def taus = _taus
      def newtaus = _newtaus

      def suc_=(suc: List[(Action, List[AgentState])]) = _suc = suc
      def taus_=(taus: List[AgentState]) = _taus = taus
      def newtaus_=(newtaus: List[AgentState]) = _newtaus = newtaus


      override
      def equals(rhs: Any) = {
        rhs match {
        case r: AgentState => {
          
          id == r.id
        }
        case _ => false
        }
      }      

      def printTopLevel() = {
        println("********** STATE **********")
        println("ID" + id + ": " + keycopy.agentString)
      }
}

object AgentState {
  private var counter: Int = 0

      def resetCounter() = counter = 0

      def mkpoly(v: Vertex): AgentState = {
  // keycopy, suc, taus, newtaus, info, id, prdiv, gldiv, mark, pid
  if (cwb.debug) println("Counter = " + counter)
  var astate = new AgentState
  astate.keycopy = v.keycopy
  astate.suc = List()
  astate.newtaus = List()
  astate.prdiv = v.keycopy.diverges()
  astate.gldiv = false
  astate.mark = false
  astate.id = counter
  astate.pid = 1

  counter += 1
  astate
}
}


object Polygraph {
  type Graphs = (AgentState, List[AgentState])

      class WeakGraph extends Exception

      var table = new HashMap[Agent, Vertex]


          /**
           *  SGraph returns the strong graph of the given agent.
           *  It is a combined version of mkweakgraph in sml.
           *  @param agent agent to have its strong graph generated.
           *  @return strong graph of the agent.
           */
          def SGraph(agent: Agent): Graphs = {
    mkGraph(false, agent)
  }


  def eqCont(item: AgentState, lst: List[AgentState]): Boolean = {
    for (l <-lst) {
      if (l.eq(item)) return true
    }
    return false
  }

  def smartPrint(asts: List[AgentState]) {
    var checkedStates = List[AgentState]()
        var statesToCheck = List[AgentState]()
        var agentsAlreadySetup = List[Agent]()

        def printOne(ast: AgentState) {
      println("STATE  " + ast.keycopy.agentString + " pid: " + ast.pid + " id: " + ast.id)
      checkedStates ++= List(ast)
      for (s<-ast.suc) {
        print(s._1.mkstr() + " -> ")
        for (s2<-s._2) print(s2.keycopy.agentString + ", ")
        println()
        for (s2 <- s._2) {
          if (!eqCont(s2, checkedStates) && !eqCont(s2, checkedStates)) {
            statesToCheck ++= List(s2)
                agentsAlreadySetup ++= List(s2.keycopy)
          }
        }
      }
    }
    for (ast<-asts) printOne(ast)



    while (!statesToCheck.isEmpty) {
      printOne(statesToCheck.head)
      statesToCheck = statesToCheck.tail
    }



  }



  /**
   * Given a tuple where the first element is an action, returns the action.
   * @param pair (action, Any)
   * @return action
   */
  def actPairToAct(pair: (Action, Any)) = pair._1


      /**
       *  WGraph returns the weak graph of the given agent.
       *  It is a combined version of mkweakgraph in sml.
       *  @param agent agent to have its weak graph generated.
       *  @return weak graph of the agent.
       */
      def WGraph(agent: Agent): Graphs = {
    mkGraph(true, agent)
  }



  /**
   * An unsafe call method for conveniently getting a vertex _known_ to be in the map.
   * Whenever called there _has_ to be an entry in the table.
   * Convenience function to prevent crazy match nesting
   * @param key agent to look up in the table.
   * @return vertex of the given agent.
   */
  def unsafeTGet(key: Agent): Vertex  = {
    table.get(key) match {
    case Some(x) => x
    case None => throw Error("BUG: Agent not defined in table!")
    }
  }


  def savewl(slist: List[AgentState]) = {
    for (s <- slist) {
      val al = for (su<-s.suc) yield {
        val (a, ls) = su
            val vlist = for (l<- ls) yield unsafeTGet(l.keycopy)
        new ActList(a, vlist)
      }
      unsafeTGet(s.keycopy).wsuc = al
    }
  }


  def mkgr(agent: Agent): Vertex = {
    def mkstate(agent: Agent): Vertex = {
        if (cwb.debug) println("enter mkstate")
        table.get(agent) match {
        case Some(v) =>  if (cwb.debug) println("exit found mkstate"); v
        case None => {
          val vr = new Vertex(agent, List(), List())
          table.put(agent, vr)
          if (cwb.debug) println("adding vertex for " + agent.agentString)

          for (trans <-agent.transitions()) {

            createLink(vr, trans)
          }
          vr
        }

        }

    }
    /**
     * createLink adds the given transition to the the given vertex. 
     * sml name: mklink
     * @param v vertex to have a transition added.
     * @param actag transition to be added.
     */
    def createLink(v: Vertex, actag: (Action, Agent)) = {
      actag match {
      case (act, ag) => 
      val vr = mkstate(ag)

      // Not sure why this is necessary, if at all.
      addLink(v, (if (act == Agent.Tau) Agent.Tau else act), vr)
      }

    }


    // TODO Watch out for object linking! Is it the same thing it was or just a copy?
    def addLink(currVert: Vertex, act: Action, v: Vertex) = {
      // action is key, suc is list. update suc with new value vref
      def actListToAct(al: ActList) = al.act
          insertListInfo(act, actListToAct, actionGE, currVert.suc) match {
        // First field holds an equal item if it exists and this is then removed from the end of the left list.
        // TODO FIX
          case (Some(x), left, right) => {
            //x.vlist = v :: x.vlist
            assert((left ++ List(x) ++ right) == currVert.suc)
            currVert.suc = left ++ List(new ActList(act, v :: x.vlist)) ++ right
          }
          case (None, left, right) => currVert.suc = left ++ List(new ActList(act, List(v))) ++ right
      }
    }
    mkstate(agent)
  }



  /**
   * Given an action which leads to a corresponding list of states.
   * Find if this action exists in the current state's suc list and if so merges.
   * Otherwise insert it as a new element (action, List[AgentState]) at the appropriate position.
   */
  def addActionSuccessors(state: AgentState, action: Action, newVal: List[AgentState]) = {
    val successors = sanitiseStateList(newVal)

        insertListInfo(action, actPairToAct, actionGE, state.suc) match {
        case (Some(x), left, right) => state.suc = left ++ List((action, mergeStateLists(x._2, successors))) ++ right
        case (None, left, right) => state.suc = left ++ List((action, successors)) ++ right
    }
  }

  def actionGE(a: Action, b: Action) = a.geAction(b)



      def order(init: AgentState, graph: HashMap[Agent,AgentState]): (AgentState, List[AgentState]) = {
    if (cwb.debug) println("In order")

    val maxid = graph.size
    if (cwb.debug) ("Max id = " + maxid)
    var A = Array.fill(maxid) {
      init
    }

    // L makes no sense in an object oriented environment.

    def upd(lst: List[(Agent, AgentState)]): Unit = {
        lst match {
        case List() => Unit
        case ((k,i)::t) => {
          graph.get(k) match {
          case Some(x) => A.update(i.id, x)
          }
          upd(t)
        }
        }
    }

    def listing(i: Int): List[AgentState] = {

        i match {
        case 0 => List(A(0))
        case n => A(n) :: listing(n-1)
        }
    } 

    // Fill the array!
    upd(graph.toList)

    // Return it as a list
    (init, listing(maxid -1))
  }

  def mkGraph(weak: Boolean, agent: Agent): Graphs = {
    val rkey = agent
        val root = mkgr(agent)



        def hashLE(ag1: (Agent, Any), ag2: (Agent, Any)) = ag1._1.hashCode <= ag2._1.hashCode
        // Creates a state map out of a vertex map
        def mkpolygraph(map: HashMap[Agent, Vertex]): HashMap[Agent,AgentState] = {
      // Previously stored separately but seems to be reset before call every time.
      // Moving into function for better maintainability
      AgentState.resetCounter()

      var stateMap = new HashMap[Agent, AgentState]
          map.toList.sortWith(hashLE) foreach {
          case (key, vertex) => stateMap.put(key, AgentState.mkpoly(vertex))
      }
      stateMap
    }

    try {
      val graph = if (weak) extractw(root) else extracts(root)
          if (cwb.debug) println("graph size = " + graph.size)


          val newg = mkpolygraph(graph)
          if (cwb.debug) println("newg size = " + newg.size)

          // now set the edge links correctly -- currently they are all nil
          setsuc(weak, graph, newg)

          // just run update..
          newg.get(rkey) match {
          case Some(x) => order(x, newg)
          }    
    } catch {
    case e: WeakGraph => {
      // Compute the weak links.
      val graph = extracts(root)
          val newg = mkpolygraph(graph)


          setsuc(false, graph, newg)


          newg.get(rkey) match {
          case Some(x) => {
            val (i, g) = obscl(order(x, newg))
                // Store the weak links.
                savewl(g)
                (i, g)
          }

          case _ => throw new Panic("Should not happen, weak graph handling!")
      }

    }
    }

  }



  /**
   * Finds a place to insert item into lst using function ge for comparison. Converts lst entry to type of item using f.
   * Returns (equalItem, left, right) where equalItem is None if no item is equal to Item.
   */
  def insertListInfo[T,K](item: K, f: T => K, ge: (K,K) => Boolean, lst: List[T]): (Option[T], List[T], List[T]) = {
      val i = lst.indexWhere (x => ge(f(x), item))
          i match {
        // Not found, elem to be inserted at the end
          case -1 => (None, lst, List())
          case _ => {
            if (f(lst(i)) == item) {
              (Some(lst(i)), lst.take(i), lst.takeRight(lst.length - i - 1))

            } else {
              (None, lst.take(i), lst.takeRight(lst.length - i))
            }
          }
      }
  }


  def stateGe(s1: AgentState, s2: AgentState): Boolean = {
      s1.id >= s2.id
  }

  def mergeStateLists(lst1: List[AgentState], lst2: List[AgentState]): List[AgentState] = {
      val vs = (lst1 ++ lst2).removeDuplicates.sortWith(stateGe)
          if (cwb.debug) for (v<-vs) v.printTopLevel()
          vs
  }


  /**
   * Returns a sorted and deduplicated version of the given AgentState list.
   * @param list list to be sanitised.
   * @return sorted and deduplicated list.
   */
  def sanitiseStateList(list: List[AgentState]): List[AgentState] = {
      val vs = list.removeDuplicates.sortWith(stateGe)
          if (cwb.debug) {
            for (v<-vs) {
              v.printTopLevel()
              print(" " + v.id)
            }
          }
      vs

  } 

  /**
   * Given a complete vx hash table and an embryonic state hash table, fill
   * in one or other of the state's successor lists, depending on weak
   * The closure operations really don't care if the successors are
   * properly ordered -- first by action and then by decreasing state
   * id -- but user's might. So sort them here: this probably isn't
   * necessary because the id's are assigned in the same sequence
   * every time, but I'm getting paranoid by now.
   * @param weak: whether to update the weak or strong state list.
   * @param graph the old graph dictionary.
   * @param newg the new graph dictionary.
   */
  def setsuc(weak: Boolean, graph: HashMap[Agent, Vertex], newg: HashMap[Agent, AgentState]) {
    def lookupold = x => graph.get(x)
        def lookupnew = x => newg.get(x)


        def newl(av: ActList): (Action, List[AgentState]) = {
            val a = av.act

                val vs = av.vlist
                var stateList: List[AgentState] = List()
                for(v <- vs) {
                  //val x = Nil
                  newg.get(v.keycopy) match {
                  case Some(x) => stateList = x :: stateList
                  case None => throw Panic("Element not found in states! newl, maybe okay")
                  }
                }
            (a, sanitiseStateList(stateList))
        }



        // TODO: Continue, define ordering etc
        /**
         * take a state, get its key, look up the corresponding vx, get its
         * successor list, turn it into a state-like list, and assign the result
         * to the state successor list. Sheesh.
         * @param state to be looked up and have its successor list updated.
         */
        def setlinks(state: AgentState) = {
            lookupold(state.keycopy) match {
            case Some(vl) =>  state.suc = for (v <- if (weak) vl.wsuc else vl.suc) yield newl(v)
            case None => throw Panic("Setlinks, item not found in map!")
            }
        }

        newg.foreach { case (ag, state) => setlinks(state) }
  }


  def extracts(root: Vertex): HashMap[Agent, Vertex] = extract(false, root)

      def extractw(root: Vertex) = {
    // TODO: Verify if (null o ! o vwsuc) root then raise WeakGraph
    if (root.wsuc == List()) {
      throw new WeakGraph;
    } else {
      extract(true, root)
    }
  }


  /**
   * build a new hash table for the trans graph root and return it, either weak
   * or strong based on boolean weak.
   * @param weak is a weak graph hash table to be created? 
   * @param root root vertex of the graph.
   * @return vertex map for weak or strong graph as specified.
   */
  def extract(weak: Boolean, root: Vertex): HashMap[Agent, Vertex] = {
    var map = new HashMap[Agent, Vertex]
        //list of vertices for each..


        // Cat returns the concatenated list of vertices from all ActList elements in the list.
        def cat(lst: List[ActList]): List[Vertex] = {
        lst match {
        case List() => List()
        case x::xs => x.vlist ++ cat(xs)
        }
        //var returnLst: List[Vertex] = List()
        //for (l <- lst) returnLst = returnLst ++ l.vlist
        //returnLst
    }

    def add(lst: List[Vertex]): Unit = {
        lst match {
        case Nil => // Do nothing
        case vr::t => {
          val keycopy = vr.keycopy
              val suc = if (weak) vr.wsuc else vr.suc
              if (cwb.debug) println("Hashval = " + keycopy.hashCode())
              if (cwb.debug) println("adding: " + keycopy.agentString)

              if (map.contains(keycopy)) {
                if (cwb.debug) println("item already added")
                add(t)
              }
              else {
                val vertices = cat(suc) ++ t
                    map.put(keycopy, vr)
                    add(vertices)
              }
        }
        }
    }
    add(List(root))
    map
  }



  // Misc commands
  type Edge = (Agent, List[(Action, Agent)])

      def graph (agent: Agent, weak: Boolean) = {

    /**
     * Reads all possible transitions out of the agent state.
     * SML name: tr
     * 
     * @param st agent state to have its transitions edges reported.
     * @return (souce agent, transition list)
     */
    def transitionLister (st: AgentState): Edge = {
        val actGentList = for ((act, slist) <- st.suc)  yield {
          // TODO: verify depth, only two layers atm, correct suc?
          for (s <- slist) yield (act, s.keycopy)
        }
        (st.keycopy, actGentList.flatten)
    }

    def makegraph(graph: Graphs): (Agent, List[Edge]) = {
      graph match {
      case (agState, stateList) => {
        if (agState.suc == List()) if (cwb.debug) println("SUC EMPTY")
        (agState.keycopy, for (state<-stateList) yield transitionLister(state))
      }
      }
    }

    // (Agent, List[Edge])
    val agentEdges = if (weak) makegraph(WGraph(agent)) else makegraph(SGraph(agent))
        if (cwb.debug) println("Finished making graphs")
        printGraph(agentEdges._1, agentEdges._2)
  }

  def printGraph (top: Agent, nodes: List[Edge]): Unit = {
    nodes match {
    case List() => ()
    case (agent, edges)::nodelist => {
      println("\n" ++ agent.agentString + "\n")
      Agent.printTransList(edges)
      printGraph(top, nodelist)
    }
    }
  }

  /**
   * reflex cl takes a graph and adds tau loops to all states.
   * @param g: graph to add tau loops to.
   * @return graph with added taus.
   */
  def reflexcl(g: Graphs): Graphs = {
    g match {
    case (init, graph) => {
      graph.foreach {
        s => addActionSuccessors(s, Agent.Tau, List(s))
      }
      (init, graph)
    }
    }
  }
  /** 
   * obscl gets a graph with P-a->Q (in the graph sense) iff P=^a=>Q.
   * @param graph: graph to be used for a weak graph structure
   * @return graph with added tau transitions. 
   */
  def obscl(graph: Graphs): Graphs = {
    val x = reflexcl(actcl(transcl(graph)))
        x
  }

  /**
   * transcl -  J. Eve & R. Kurki-Suonio
   * @param g graph to be transformed.
   * @return transformed graph.
   */
  def transcl(g: Graphs): Graphs = {
    g match {
    case (init, graph) => {
      sanityCheck(graph)
      val sz = graph.head.id + 1
      val starray = Array.fill(sz) {
        init
      }
      var listindex = sz
          var stacktop = -1
          var i = 0
          val j = 0
          val vertices = Array.fill(sz) {
        -1
      }
      val index = Array.fill(sz) {
        -1
      }

      def stateGE(stateA: AgentState, stateB: AgentState) = stateA.id >= stateB.id

          /**
           *  inits puts the given state into the array, set its newtaus field to nil, set its
           *  taus field to be the tau-list from its successor list. (Why?)
           *  @param state state to be put into the array.
           */
          def inits(state: AgentState) = {
          starray(state.id) = state
              state.newtaus = Nil
              setTausFromSuccessors(state)
      }

      def actExtracter(item :(Action, List[AgentState])) = item._1

          /**
           * afters updates both the taus field and the taus part of the successor list
           * from newtaus, if there are any newtaus. There'll be an uncaught
           * exception Noacts if afters is called on a state with no
           * tau-successors?! It had better not be...
           * @param state: state to have its taus fields set
           */
          def afters(state: AgentState) = {
          if (state.newtaus != Nil) {
            state.taus = state.newtaus
                class Noacts extends Exception
                val tau = Agent.Tau

                for (t <- state.taus) {
                  // t.printState()
                }
            insertListInfo(tau,actExtracter, actionGE, state.suc) match {
              // TODO verify sanity
            case (Some(x), left ,right) => state.suc = left ++ List((tau, state.taus)) ++ right
            case _ => throw new Noacts
            }



            //            for (i <- 0 until state.suc.length) {
            //              val s = state.suc(i)
            //              
            //              
            //              
            //              
            //              if (s._1 == Tau) {
            //                state.
            //              }
            //            }

            //   tauRef(state.suc) // TODO Assignment or equivalent!!
          }
      }


      /** Given two states, add the tau-successors of the second into the first
       * one's tau-successor list.
       * sml name: add_taus
       * @param stateA state to have taus added
       * @param stateB state to pull taus from
       */
      def addTaus(stateA: AgentState, stateB: AgentState) {
        stateA.newtaus = (stateA.newtaus ++ stateB.newtaus).sortWith(stateGE).removeDuplicates
      }


      def closure(state: AgentState): Unit = {
          var wList = List[AgentState]()
              var wId = 0
              var w = init

              stacktop += 1
              index(state.id) = stacktop
              vertices(stacktop) = state.id
              wList = state.taus

              for (w<-wList) { 
                //while (wList != List()) {
                //w = wList.head
                wId = w.id
                    state.newtaus = (w :: state.newtaus).sortWith(stateGE).removeDuplicates
                    if (index(wId) == -1) closure(w)

                    if(index(wId) <= stacktop) {
                      // Orig updateArray(index,id,
                      //                            Int.min(index sub id,
                      //                                    index sub (!w_id)))
                      if (index(wId) < index(state.id)) {
                        index(state.id) = index(wId)
                      }
                    } else  {
                      addTaus(state, starray(vertices(index(wId))))
                    }
                // TODO verify whether inside or outside else.
                //wList = wList.tail            
              }
          if (cwb.debug) println(state.keycopy.agentString + " new taus: " + state.newtaus)
          if (state.id == vertices(index(state.id))) {
            listindex -= 1
                wId = vertices(stacktop)
                w = starray(wId)
                stacktop -= 1
                index(wId) = listindex
                while (wId != state.id) {
                  addTaus(state, w)
                  wId = vertices(stacktop)
                  w = starray(wId)
                  stacktop -= 1
                  index(wId) = listindex
                }
            vertices(listindex) = state.id
          }
      }

      graph.foreach {
        g => inits(g)
      }

      i = 0
          while (i < sz) {
            if (index(i) == -1) closure(starray(i))
            i += 1
          }
      i = 0

          while (i < sz) {
            val j = vertices(index(i))
                if (i != j) {
                  addTaus(starray(i), starray(j))
                }
            i += 1
          }

      graph.foreach {
        g => afters(g)
      }

      (init, graph)
    }
    }




  }


  def getActionSuccessors (stateAct: (AgentState, Action)): List[AgentState] = {
    stateAct match {
    case (state, action) => {
      val i = state.suc.indexWhere(x => x._1 == action)
          if (i == -1) List()
          else state.suc(i)._2
    }
    }
  }


  def setTausFromSuccessors(state: AgentState) = {
    state.taus = getActionSuccessors((state, Agent.Tau))
  }



  def sanityCheck(stateList: List[AgentState]) = {
    def f(states: List[AgentState]): Unit = {
        states match {
        case List() => ()
        case List(_) => ()
        case (a::b::t) => {
          if (a.id > b.id) f(b::t)
          else throw new Panic("sanityCheck says we're insane!")
        }
        }
    }
    f(stateList)
  }




  /**
   * actcl replaces -a-> by ==>-a->==>  (for a#tau) on the given graph
   * It is assumed that the tau field in each state has been set by transcl.
   * @param g graph to add weak transitions to.
   * @returns modified graph.
   */
  def actcl(g: Graphs): Graphs = {
    g match {
    case (init, graph) => {
      var temp: List[(Action, Array[Boolean])] = List()
          val sz = graph.head.id + 1
          val stArray = Array.fill(sz) {init}


    val i = 0

        /**
         *  updateAll: given an array and a list of states,
         *  sets the array elements indexed by ids of states in the state list to true
         *  @param a array to be updated
         *  @param stateList list of states to have its ids set in the array.
         */

        def updateAll(a: Array[Boolean], stateList: List[AgentState]) {
      stateList foreach {
        state => a(state.id) = true
      }
    }

    def findActInTemp(ac: Action, abs: List[(Action, Array[Boolean])]): Array[Boolean] = {
        abs match { 
        case List() => {
          val arr = Array.fill(sz) {false}
          temp = (ac, arr) :: temp
              arr
        }
        case (act, arr)::t => {
          if (ac == act) arr else findActInTemp(ac, t)
        }
        }
    }

    def clear(arrpair: (Any, Array[Boolean])) = {
      arrpair match {
      case (_, arr) => for (i <- 0 until sz)  arr(i) = false
      }
    }

    def addSuc(state: AgentState, abr: (Action, Array[Boolean])): Unit = {
      abr match {
      case (ac, arr) => {
        var l = List[AgentState]()

            //val listarr: List[AgentState] = {
            for (i <- 0 until sz) {
              if (arr(i)) l = stArray(i) :: l
            }

        val listarr = l

            if (listarr.isEmpty) Unit
            else {

              insertListInfo(ac, actPairToAct, actionGE, state.suc) match {
                // Either insert in correct position or have it automatically replace the equal atc.
              case (_, left, right) => state.suc = left ++ List((ac, listarr)) ++ right
                  // case (Some(x), left, right) => state.suc = left ++ List((ac, listarr)) ++ right
              }
            }


      }
      }
    }


    def beginState(state: AgentState) = {
      def collectTaus(arr: Array[Boolean], states: List[AgentState]) = {
        states.foreach {
          s => updateAll(arr, s.taus)
        }
      }

      def oneAct(item: (Action, List[AgentState])) = {
        item match {
        case (Agent.Tau, l) => Unit
        case (ac, l) => collectTaus(findActInTemp(ac, temp), l)
        }
      }


      temp.foreach {
        t => clear(t)
      }

      state.suc.foreach {
        s => oneAct(s)
      }

      temp.foreach {
        t => addSuc(state, t)
      }
    }

    def finishState(state: AgentState) = {
      def oneAct(item: (Action, List[AgentState])) = {
        item match {
        case (Agent.Tau, l) => ()
        case (ac, l) => updateAll(findActInTemp(ac, temp), l)
        }
      }

      def collectsuc(state: AgentState) = {
        state.suc.foreach {
          s => oneAct(s)
        }
      }
      temp.foreach {
        t => clear(t)
      }

      (state::state.taus).foreach {
        s => collectsuc(s)
      }

      temp.foreach {
        t => addSuc(state, t)
      }
    }

    graph.foreach {
      g => stArray(g.id) = g
    }

    graph.foreach {
      g => beginState(g)
    }

    graph.foreach {
      g => finishState(g)
    }
    (init, graph)
    }
    }
  }
}





object GraphCommand extends Command {
  val name = "graph"
      val helpShort = "list the transition graph of an agent"
      val helpDetailed = "graph A;" +
          "\nSimple-mindedly, and not particularly efficiently, calculates the whole" +
          "\ntransition graph of the agent. You do not want to do this for large agents," +
          "\n let alone infinite ones!" +
          "\n" +
          "\n Because of a feature of how graphs are calculated and stored, internal" +
          "\n actions don't show what communication they come from (in CCS, you see tau," +
          "\n  never tau<a>). Use \"transitions\" to get this information when you want it."
          /**
           * Reads the given string input as an agent, generates its strong graph and
           * displays it to the user.
           * @param input string representation of an agent.      
           */
           def apply(input: String) = {
    val parser = Agent.parser
        val agent = parser.readAgent(input)
        Polygraph.graph(agent, false)
  }
}

object WGraphCommand extends Command {
  val name = "wgraph"
      val helpShort = "list the weak transition graph of an agent"
      val helpDetailed = "wgraph A;" +
          "\nSimple-mindedly, and not particularly efficiently, calculates the whole" +
          "\ntransition graph of the agent. You do not want to do this for large agents," +
          "\n let alone infinite ones!" +
          "\n" +
          "\n Because of a feature of how graphs are calculated and stored, internal" +
          "\n actions don't show what communication they come from (in CCS, you see tau," +
          "\n  never tau<a>). Use \"transitions\" to get this information when you want it."
          /**
           * Reads the given string input as an agent, generates its weak graph and
           * displays it to the user.
           * @param input string representation of an agent.      
           */       
           def apply(input: String) = {
    val parser = Agent.parser
        val agent = parser.readAgent(input)
        Polygraph.graph(agent, true)
  }
}


object SizeCommand extends Command {
  val name = "size"
      val helpShort = "find the number of states of a finite-state agent"
      val helpDetailed = "The number of states of an agent is not as clear a concept as you might" +
          "\nthink: treat the number as a rough indication of size, only."
          val parser = Agent.parser

          def apply(input: String) = {
    val agent = parser.readAgent(input)
        val gr = Polygraph.SGraph(agent)
        val num_states = gr._2.head.id + 1
        val ending = if (num_states != 1) "s." else "."
          println(agent.agentString + " has " + num_states + " state" + ending)
  }
}